package project;

import com.sun.org.apache.xerces.internal.parsers.DOMParser;
import java.io.FileNotFoundException;
import java.io.IOException;

import java.util.logging.Level;
import java.util.logging.Logger;
import javax.xml.parsers.DocumentBuilderFactory;
import javax.xml.parsers.DocumentBuilder;
import javax.xml.parsers.ParserConfigurationException;
import javax.xml.xpath.XPathExpressionException;
import org.w3c.dom.Document;
import org.w3c.dom.NodeList;
import org.w3c.dom.Node;
import org.w3c.dom.Element;
import java.io.File;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import javax.xml.xpath.XPathConstants;
import javax.xml.xpath.XPathExpression;
import javax.xml.xpath.XPathFactory;
import org.xml.sax.SAXException;

enum Type {

    atomic, top, bottom, and, or, not, all, exists
};

class Abox {
}

class ALC extends Abox {

    Type type;
    String name;
    ALC left, right;
    Role child;
}

class Role extends Abox {

    String name;
    String ind1;
    String ind2;
}

class Tbox {

    Type type;
    String name;
    Tbox left, right;
}

class Gedge {

    String name;
    Gnode adj;
}

class Gnode {

    static int nnum = 1;
    String name;
    LinkedList<ALC> nodelabel = new LinkedList<ALC>();
    LinkedList<ALC> nodenplabel = new LinkedList<ALC>();
    LinkedList<Gedge> edgelist = new LinkedList<Gedge>();
    LinkedList<Gnode> parentlist = new LinkedList<Gnode>();

    @Override
    protected Gnode clone() {
        Gnode newnode = new Gnode();
        newnode.name = name;
        newnode.nodelabel = (LinkedList<ALC>) nodelabel.clone();
        newnode.nodenplabel = (LinkedList<ALC>) nodenplabel.clone();
        newnode.edgelist = (LinkedList<Gedge>) edgelist.clone();
        newnode.parentlist = (LinkedList<Gnode>) parentlist.clone();

        return newnode;
    }
}

public class Project implements Runnable {

    HashMap alcInd = new HashMap<ALC, String>();
    //Thread t;
    
    //private static final ThreadLocal < Thread > uniqueNum = 
      //   new ThreadLocal < Thread > () ;
    
    List tArray = new LinkedList<Thread>();
    HashMap tSibling = new HashMap<Thread, List<Thread>>();
    HashMap tValue = new HashMap<Thread, Boolean>();
    HashMap tList = new HashMap<Thread, LinkedList<Gnode>>();
    //LinkedList<Gnode> childListNode = null;
    
    static int tNum = 0;

    void correctSpace(Document doc) throws XPathExpressionException {
        XPathFactory xpathFactory = XPathFactory.newInstance();
// XPath to find empty text nodes.
        XPathExpression xpathExp = xpathFactory.newXPath().compile(
                "//text()[normalize-space(.) = '']");
        NodeList emptyTextNodes = (NodeList) xpathExp.evaluate(doc, XPathConstants.NODESET);

// Remove each empty text node from document.
        for (int i = 0; i < emptyTextNodes.getLength(); i++) {
            Node emptyTextNode = emptyTextNodes.item(i);
            emptyTextNode.getParentNode().removeChild(emptyTextNode);
        }

    }
    List aboxL = new LinkedList<Abox>();
    List tboxL = new LinkedList<Tbox>();

    private static String getTagValue(String sTag, Element eElement) {
        NodeList nlList = eElement.getElementsByTagName(sTag).item(0).getChildNodes();

        Node nValue = (Node) nlList.item(0);

        return nValue.getNodeValue();
    }

    void createRole(Role role, Node node) {
        role.name = node.getFirstChild().getNodeValue().replace("\n", "");
    }

    void createALC(ALC alcC, Node node) {

        Node alc1 = node.getFirstChild();
        // System.out.println("alc child " + alc1.getNodeName() + " " + alc1.getNodeValue());
        if (alc1.getNodeName().equals("atomic")) {
            alcC.type = Type.atomic;
            // System.out.println("Reached atomic "+alc1.getFirstChild().getNodeValue());
            alcC.name = alc1.getFirstChild().getNodeValue().replace("\n", "");

        } else if (alc1.getNodeName().equals("top")) {
            alcC.type = Type.top;
            alcC.name = "top";
        } else if (alc1.getNodeName().equals("bottom")) {
            alcC.type = Type.bottom;
            alcC.name = "bottom";
        } else if (alc1.getNodeName().equals("and")) {
            alcC.type = Type.and;
            alcC.name = "and";
            alcC.left = new ALC();
            alcC.right = new ALC();
            createALC(alcC.left, alc1.getFirstChild());
            createALC(alcC.right, alc1.getFirstChild().getNextSibling());

        } else if (alc1.getNodeName().equals("or")) {
            alcC.type = Type.or;
            alcC.name = "or";//alc1.getFirstChild().getNodeValue().replace("\n", "");
            alcC.left = new ALC();
            alcC.right = new ALC();
            createALC(alcC.left, alc1.getFirstChild());
            createALC(alcC.right, alc1.getFirstChild().getNextSibling());

        } else if (alc1.getNodeName().equals("not")) {
            alcC.type = Type.not;
            alcC.name = "not";//alc1.getFirstChild().getNodeValue().replace("\n", "");
            alcC.left = new ALC();
            createALC(alcC.left, alc1.getFirstChild());

        } else if (alc1.getNodeName().equals("all")) {
            alcC.type = Type.all;
            alcC.name = "all";//alc1.getFirstChild().getNodeValue().replace("\n", "");
            alcC.child = new Role();
            alcC.left = new ALC();

            // alcC.child.ind1 = node.getNextSibling().getFirstChild().getNodeValue().replace("\n", "");
            //alcC.child.ind2 = node.getNextSibling().getNextSibling().getFirstChild().getNodeValue().replace("\n", "");

            createRole(alcC.child, alc1.getFirstChild());
            createALC(alcC.left, alc1.getFirstChild().getNextSibling());


        } else if (alc1.getNodeName().equals("exists")) {
            alcC.type = Type.exists;
            alcC.name = "exists";//alc1.getFirstChild().getNodeValue().replace("\n", "");
            alcC.child = new Role();
            alcC.left = new ALC();
            createRole(alcC.child, alc1.getFirstChild());
            createALC(alcC.left, alc1.getFirstChild().getNextSibling());


        }
    }

    void parseXML(String fileName) throws FileNotFoundException, ParserConfigurationException, SAXException, IOException {
        DOMParser parser = new DOMParser();
//parser.setPreserveWhitespace(false);

        File fXmlFile = new File(fileName);
        DocumentBuilderFactory dbFactory = DocumentBuilderFactory.newInstance();
        //dbFactory.setIgnoringElementContentWhitespace(true);
        DocumentBuilder dBuilder = dbFactory.newDocumentBuilder();

        Document doc = dBuilder.parse(fXmlFile);
        try {
            correctSpace(doc);
            //doc.getDocumentElement().normalize();
        } catch (XPathExpressionException ex) {
            Logger.getLogger(Project.class.getName()).log(Level.SEVERE, null, ex);
        }

        System.out.println("Root element :" + doc.getDocumentElement().getNodeName());

        NodeList nList = doc.getElementsByTagName("abox");



        System.out.println("-----------------------");


        for (int temp = 0; temp < nList.getLength(); temp++) {

            Node nNode = nList.item(temp);
            System.out.println(nNode.getNodeName());
            //if (nNode.getNodeType() == Node.ELEMENT_NODE) 



            Node aboxHead = nNode.getFirstChild();
            if (aboxHead.getNodeName().equals("alc")) {

                ALC alc = new ALC();
                //Whether this is correct
                alcInd.put(alc, aboxHead.getNextSibling().getFirstChild().getNodeValue());
                // alc.ind1 = aboxHead.getNextSibling().getFirstChild().getNodeValue();
                aboxL.add(alc);
                createALC(alc, aboxHead);



            } else if (aboxHead.getNodeName().equals("role")) {

                Role role = new Role();
                aboxL.add(role);
                role.ind1 = aboxHead.getNextSibling().getFirstChild().getNodeValue().replace("\n", "");
                role.ind2 = aboxHead.getNextSibling().getNextSibling().getFirstChild().getNodeValue().replace("\n", "");

                createRole(role, aboxHead);

            }

        }
        NodeList nList1 = doc.getElementsByTagName("tbox");



        System.out.println("-----------------------");


        for (int temp = 0; temp < nList1.getLength(); temp++) {

            Node nNode = nList1.item(temp);
            System.out.println(nNode.getNodeName());
            //if (nNode.getNodeType() == Node.ELEMENT_NODE) 


            Node tboxHead = nNode.getFirstChild();
            if (tboxHead.getNodeName().equals("alc")) {

                ALC alc = new ALC();
                tboxL.add(alc);
                createALC(alc, tboxHead);

            }


        }


    }

    /**
     * @param args the command line arguments
     */
    public static void main(String[] args) throws FileNotFoundException, InterruptedException {
        // TODO code application logic here
        String fileName = args[0];
        Project myProject = new Project();
        try {
            myProject.parseXML(args[0]);
        } catch (ParserConfigurationException ex) {
            Logger.getLogger(Project.class.getName()).log(Level.SEVERE, null, ex);
        } catch (SAXException ex) {
            Logger.getLogger(Project.class.getName()).log(Level.SEVERE, null, ex);
        } catch (IOException ex) {
            Logger.getLogger(Project.class.getName()).log(Level.SEVERE, null, ex);
        }
        myProject.initialization();
        //List<Gnode> lg = new LinkedList<Gnode>(myProject.nodes.values());
        //myProject.tableau((LinkedList<Gnode>)myProject.nodes.values());
        if (myProject.tableau(myProject.listNode)) {
            System.err.println("Satisfiable....");
        } else {
            System.err.println("Not Satisfiable.......");
            System.exit(0);
        }

    }
    HashMap<String, Gnode> nodes = new HashMap<String, Gnode>();
    LinkedList<Gnode> listNode = null;
    LinkedList<Gnode> childListNode = null;
    //boolean childValue = true;
    //LinkedList<Gnode> listNodeR = null;

    void initialization() {
        //System.out.println("aboxL.size = "+aboxL.size());
        for (int i = 0; i < aboxL.size(); i++) {

            if (aboxL.get(i) instanceof ALC) {
                // System.out.println("aboxL ALC = "+i);
                Gnode newnode = new Gnode();
                String name = alcInd.get((ALC) aboxL.get(i)).toString().replace("\n", "");
                newnode.name = name;
                if (!nodes.containsKey(name)) {
                    nodes.put(name, newnode);
                }
                nodes.get(name).nodelabel.add((ALC) aboxL.get(i));
                System.out.println("name in init " + name + " label: " + ((ALC) aboxL.get(i)).name);

            } else if (aboxL.get(i) instanceof Role) {
                //System.out.println("aboxL Role = "+i);
                Gnode newnode1 = null;
                String name1 = ((Role) aboxL.get(i)).ind1;
                if (!nodes.containsKey(name1)) {
                    newnode1 = new Gnode();
                    newnode1.name = name1;
                    nodes.put(name1, newnode1);
                } else {
                    newnode1 = nodes.get(name1);
                }

                Gnode newnode2 = null;//new Gnode();
                String name2 = ((Role) aboxL.get(i)).ind2;
                if (!nodes.containsKey(name2)) {
                    newnode2 = new Gnode();
                    newnode2.name = name2;
                    nodes.put(name2, newnode2);
                } else {
                    newnode2 = nodes.get(name2);
                }


                Gedge edge = new Gedge();
                edge.name = ((Role) aboxL.get(i)).name;
                edge.adj = newnode2;
                System.out.println("Edge name " + edge.name + " Node " + newnode1.name);
//                 System.out.println("nodelabel james "+listNode.get(1).name +" label: "+listNode.get(1).nodelabel.size());
// System.out.println("nodelabel james edge "+newnode2.name +" label: "+newnode2.nodelabel.size());
//System.out.println("nodelabel james edge from hash "+nodes.get("jamespotter").name +" label: "+nodes.get("jamespotter").nodelabel.size());

                newnode1.edgelist.add(edge);

                newnode2.parentlist.add(newnode1);



                /*if (!nodes.containsKey(name1)) {
                nodes.put(name1, newnode1);
                }
                if (!nodes.containsKey(name2)) {
                nodes.put(name2, newnode2);
                }
                 */

            }
        }


        //  System.out.println("nodelabel james edge from hash "+nodes.get("jamespotter").name +" label: "+nodes.get("jamespotter").nodelabel.size());

        listNode = new LinkedList<Gnode>(nodes.values());
        //System.out.println("nodelabel james after edge "+listNode.get(0).edgelist.get(0).adj.name +" label: "+listNode.get(0).edgelist.get(0).adj.nodelabel.size());

        //System.out.println("nodelabel james "+listNode.get(1).name +" label: "+listNode.get(1).nodelabel.size());

        //   System.out.println("Edgelist size 0 = "+listNode.get(0).edgelist.size());
        for (int i = 0; i < listNode.size(); i++) {
            for (int j = 0; j < tboxL.size(); j++) {
                //listNode.get(i).nodelabel.add(tboxL.get(j));
                listNode.get(i).nodelabel.add((ALC) tboxL.get(j));
            }
            listNode.get(i).nodenplabel = (LinkedList<ALC>) listNode.get(i).nodelabel.clone();
        }
        //System.out.println("nodelabel james "+listNode.get(1).name +" label: "+listNode.get(1).nodelabel.size());



    }

    Boolean checkSibling(Thread current) throws InterruptedException {
        if (tSibling.get(current) != null) {

            return true;

        } else {
            return false;
        }
    }

    Boolean siblingValue(Thread current) throws InterruptedException {
        List<Thread> siblingList = (List<Thread>)tSibling.get(current);
        Boolean rValue = true;
        for(int i = 0; i < siblingList.size(); i++)
        {
            
            ((Thread) siblingList.get(i)).join();
            
            System.out.println("i = "+i+ " "+current.toString()+((Thread) siblingList.get(i)).toString()+" value "+((Boolean) tValue.get((Thread) siblingList.get(i))));
       
            synchronized(this){
            if((Boolean) tValue.get((Thread) siblingList.get(i)) == false)
            {
                rValue = false;
            }
            }
            
        }
        return rValue;
        //((Thread) tSibling.get(current)).join();
        //System.out.println(current.toString()+((Thread) tSibling.get(current)).toString()+" value "+((Boolean) tValue.get((Thread) tSibling.get(current))));
        //return (Boolean) tValue.get((Thread) tSibling.get(current));

    }
    
    
    synchronized int getTNum ()
    {
        tNum++;
        return tNum;
        
        
    }

     boolean  tableau(LinkedList<Gnode> listNod) throws InterruptedException {




        //boolean hasChild = false;
        if(listNod == null)
        {
            try {
                tValue.put(Thread.currentThread(), false);
                System.out.println("\n\n\nNull list+\n\n\n\n");
                System.out.println("\n");
                byte []b = new byte[80];
                //System.in.read(b);
                //System.exit(0);
                return true;
            } catch (Exception ex) {
                Logger.getLogger(Project.class.getName()).log(Level.SEVERE, null, ex);
            }
        }
        Thread t = null;
        LinkedList<Gnode> listNodeR = null;
        for (int i = 0; i < listNod.size(); i++) {
            // System.out.println("nodelabel james "+listNod.get(1).name +" label: "+listNod.get(1).nodelabel.size());

            boolean bflag = false;
            System.out.println("Inside tableau " + i);
            System.out.println("Inside tableau: nodenplabel size = " + listNod.get(i).nodenplabel.size());

            for (int j = 0; j < listNod.get(i).nodenplabel.size(); j++) {
                //     System.out.println("j = "+j+" total = "+listNod.get(i).nodenplabel.size());
                bflag = false;
                ALC cnode = listNod.get(i).nodenplabel.get(j);
                // System.out.println("Inside j tableau " + j+cnode.type);
                if (cnode.type == Type.and) {
                    listNod.get(i).nodenplabel.add(cnode.left);
                    System.out.println("Add left in And of type: " + cnode.left.name);
                    listNod.get(i).nodelabel.add(cnode.left);
                    if (checkContradiction(listNod.get(i).nodelabel, cnode.left) == true) {
                        System.out.println(Thread.currentThread().toString()+" Satisfiable and...");
                        Boolean rValue = false;
                        if (checkSibling(Thread.currentThread())) {
                            rValue = siblingValue(Thread.currentThread());
                        } else {
                            rValue = true;
                        }
                         synchronized(this){
                        tValue.put(Thread.currentThread(), rValue);
                        return rValue;
                        }


                        //return true;
                    }
                    listNod.get(i).nodenplabel.add(cnode.right);
                    listNod.get(i).nodelabel.add(cnode.right);
                    System.out.println("Add right in And of type: " + cnode.right.name);
                    if (checkContradiction(listNod.get(i).nodelabel, cnode.right) == true) {
                        System.out.println(Thread.currentThread().toString()+" Satisfiable and...");
                        Boolean rValue = false;
                        if (checkSibling(Thread.currentThread())) {
                            rValue = siblingValue(Thread.currentThread());
                        } else {
                            rValue = true;
                        }
                        synchronized(this){
                        tValue.put(Thread.currentThread(), rValue);
                        return rValue;
                        }

                    }
                    //System.out.println("Before rem in and = " + listNode.get(i).nodenplabel.size());

                    listNod.get(i).nodenplabel.remove(j);
                    //System.out.println("After rem in and = " + listNode.get(i).nodenplabel.size());
                    // System.exit(0);
                }

            }
            
            
            for (int j = 0; j < listNod.get(i).nodenplabel.size(); j++) {
                ALC cnode = listNod.get(i).nodenplabel.get(j);
                if (cnode.type == Type.or) {
                    boolean rec = false;
                    // System.out.println("Inside j tableau or " + j);
                    if (checkContradiction(listNod.get(i).nodelabel, cnode.left) == true) {
                        if (checkContradiction(listNod.get(i).nodelabel, cnode.right) == true) {
                            //           System.out.println("Satisfiable or...");
                            Boolean rValue = false;
                            if (checkSibling(Thread.currentThread())) {
                                rValue = siblingValue(Thread.currentThread());
                            } else {
                                rValue = true;
                            }
                            synchronized(this){
                        tValue.put(Thread.currentThread(), rValue);
                        return rValue;
                        }

                        } else {
                            listNod.get(i).nodenplabel.add(cnode.right);
                            listNod.get(i).nodelabel.add(cnode.right);

                            bflag = true;
                        }
                    } else {
                        if (checkContradiction(listNod.get(i).nodelabel, cnode.right) == true) {
                            listNod.get(i).nodenplabel.add(cnode.left);
                            listNod.get(i).nodelabel.add(cnode.left);
                            bflag = true;
                        } else {

                            //  System.out.println("nplist size = "+listNod.get(i).nodenplabel.size());


                            listNod.get(i).nodenplabel.remove(j);
                            //  System.out.println("nplist size after rem = "+listNod.get(i).nodenplabel.size());

                           listNodeR = new LinkedList<Gnode>();
                            for (int kj = 0; kj < listNod.size(); kj++) {
                                listNodeR.add(listNod.get(kj).clone());
                            }


                            listNod.get(i).nodelabel.add(cnode.left);
                            System.out.println("Add left in Or of type: " + cnode.left.name);
                            listNod.get(i).nodenplabel.add(cnode.left);


                            //System.out.println("nplist size = "+listNod.get(i).nodenplabel.size());


                            listNodeR.get(i).nodelabel.add(cnode.right);
                            System.out.println("Add right in Or of type: " + cnode.right.name);
                            listNodeR.get(i).nodenplabel.add(cnode.right);
                            //System.exi
                            //  System.out.println("nplist size = "+listNod.get(i).nodenplabel.size());
                            bflag = true;

                            System.out.println("Recursion started " + cnode.right.name);
                            /*  if (hasChild) {
                            t.join();
                            }*/
                            /*    if (!hasChild && !childValue) {
                            return false;
                            }*/


                            /*boolean rValue = checkSibling(Thread.currentThread());
                            tValue.put(Thread.currentThread(), rValue);
                            return rValue;*/



                           
                           // childListNode = listNodeR;
                            //   hasChild = true;
                            // System.out.println("New thread...\n....\n\n..");
                           if(listNodeR != null){
                               
                              if(getTNum() < 10) 
                              {
                               
                           t = new Thread(this, "ORRight"+getTNum());
                           //tNum++;
                           synchronized(this){
                           tList.put(t, listNodeR);}
                            List<Thread> siblingList = null;
                            if(tSibling.get(Thread.currentThread()) == null)
                            {
                               siblingList = new LinkedList<Thread>();
                            }
                            else
                            {
                                siblingList = (List<Thread>)tSibling.get(Thread.currentThread());
                            }
                            
                            siblingList.add(t);
                            
                            tSibling.put(Thread.currentThread(), siblingList);
                            
                            //System.out.println(Thread.currentThread().toString()+" has child as "+t.toString());
                            
                            //tArray.add(t);
                            
                            
                            //System.out.println(t.toString()+" has values as (before run) "+tList.get(t));

                            
//                            t = new Thread();
                           // if(t.getState() == Thread.State.RUNNABLE)
                            t.start();
                              }
                              else{

                            if(tableau(listNodeR) == false)//Not-satisfiable
                            {
                            System.err.println("Recursion ended false\nSatisfiable\n");
                            return false;
                            }
                              }
                            //  t.join();

                           // System.out.println("Recursion ended with childvalue" + childValue);
                           }
                            rec = true;
                        }

                    }
                    if (!rec) {
                        // System.out.println("Before rem in or = " + listNode.get(i).nodenplabel.size());

                        listNod.get(i).nodenplabel.remove(j);
                        //System.out.println("After rem in or = " + listNode.get(i).nodenplabel.size());
                    }
                    //System.exit(0);
                }

            }
            if (bflag) {
                i--;
                continue;
            }

            for (int j = 0; j < listNod.get(i).nodenplabel.size(); j++) {
                ALC cnode = listNod.get(i).nodenplabel.get(j);
                if (cnode.type == Type.exists) {
                    System.out.println("Inside j tableau exists " + j);
                    System.out.println(listNod.get(i).edgelist.size());
                    for (int k = 0; k < listNod.get(i).edgelist.size(); k++) {
                        if (listNod.get(i).edgelist.get(k).name.equals(cnode.child.name)) {
                            Gnode node1 = listNod.get(i).edgelist.get(k).adj;
                            if (searchLabel(node1, cnode.left) == false) {
                                System.out.println("New node created in exists after search");
                                Gnode newnode = new Gnode();
                                newnode.name = "v" + Gnode.nnum;
                                Gnode.nnum = Gnode.nnum + 1;
                                newnode.nodelabel.add(cnode.left);
                                newnode.nodenplabel.add(cnode.left);
                                Gedge newedge = new Gedge();
                                newedge.name = cnode.child.name;
                                newedge.adj = newnode;
                                for (int kj = 0; kj < tboxL.size(); kj++) {
                                    //listNode.get(i).nodelabel.add(tboxL.get(j));
                                    newnode.nodelabel.add((ALC) tboxL.get(kj));
                                }
                                newnode.parentlist.add(listNod.get(i));
                                listNod.get(i).edgelist.add(newedge);
                                listNod.add(newnode);

                            } else {
                                System.out.println("Search label true in exists");
                            }
                        } else {
                            System.out.println("New node created in exists else");
                            Gnode newnode = new Gnode();
                            newnode.name = "v" + Gnode.nnum;
                            Gnode.nnum = Gnode.nnum + 1;
                            newnode.nodelabel.add(cnode.left);
                            newnode.nodenplabel.add(cnode.left);
                            Gedge newedge = new Gedge();
                            newedge.name = cnode.child.name;
                            newedge.adj = newnode;
                            newnode.parentlist.add(listNod.get(i));
                            for (int kj = 0; kj < tboxL.size(); kj++) {
                                //listNode.get(i).nodelabel.add(tboxL.get(j));
                                newnode.nodelabel.add((ALC) tboxL.get(kj));
                            }
                            listNod.get(i).edgelist.add(newedge);
                            listNod.add(newnode);
                        }
                    }

                }
                // System.out.println("Before rem in exists = " + listNode.get(i).nodenplabel.size());

                listNod.get(i).nodenplabel.remove(j);
                //  System.out.println("After rem in exists = " + listNode.get(i).nodenplabel.size());
                //System.exit(0);
            }
            for (int j = 0; j < listNod.get(i).nodenplabel.size(); j++) {
                ALC cnode = listNod.get(i).nodenplabel.get(j);
                if (cnode.type == Type.all) {
                    System.out.println("Inside j tableau all " + j);
                    //System.out.println("nodelabel james "+listNod.get(1).name +" label: "+listNod.get(1).nodelabel.size());

                    for (int k = 0; k < listNod.get(i).edgelist.size(); k++) {
                        if (listNod.get(i).edgelist.get(k).name.equals(cnode.child.name)) {
                            Gnode node1 = listNod.get(i).edgelist.get(k).adj;
                            //System.out.println("is james "+node1.name);

                            if (searchLabel(node1, cnode.left) == false) {
                                //System.out.println("cnode.left "+cnode.left.name);
                                //System.out.println("cnode.left.left "+cnode.left.left.name);
                                // System.out.println("james has "+node1.nodelabel.size());
                                if (checkContradiction(node1.nodelabel, cnode.left)) {
                                    System.out.println(Thread.currentThread().toString()+" Satisfiable all...");
                                    Boolean rValue = false;
                                    if (checkSibling(Thread.currentThread())) {
                                        rValue = siblingValue(Thread.currentThread());
                                    } else {
                                        rValue = true;
                                    }
                                     synchronized(this){
                        tValue.put(Thread.currentThread(), rValue);
                        return rValue;
                        }




                                } else {
                                    System.out.println(Thread.currentThread().toString()+" no contr in all");
                                }
                                node1.nodelabel.add(cnode.left);
                                node1.nodenplabel.add(cnode.left);

                            }
                        }
                    }
                    // System.out.println("Before rem in all = " + listNode.get(i).nodenplabel.size());

                    listNod.get(i).nodenplabel.remove(j);
                    //System.out.println("After rem in all = " + listNode.get(i).nodenplabel.size());
                    //System.exit(0);
                }
            }
            if (listNod.get(i).name.charAt(0) == 'v') {
                for (int z = 0; z < listNod.get(i).parentlist.size(); z++) {
                    if (checkSubset(listNod.get(i).parentlist.get(z), listNod.get(i)) == true) {
                        System.out.println(Thread.currentThread().toString()+" Satisfiable...");
                        Boolean rValue = false;
                        if (checkSibling(Thread.currentThread())) {
                            rValue = siblingValue(Thread.currentThread());
                        } else {
                            rValue = true;
                        }
                        synchronized(this){
                        tValue.put(Thread.currentThread(), rValue);
                        return rValue;
                        }

                    }
                }
            }
        }
        //System.out.println("Satisfiable...");  
        Boolean rValue = false;
       // if (checkSibling(Thread.currentThread())) {
         //   rValue = siblingValue(Thread.currentThread());
        //} 

        //else
        synchronized(this)
        {
            rValue = false;
            System.err.println(" Not Satisfiable\n\n");
            System.exit(0);
            
            
        }
        
        System.out.println(Thread.currentThread().toString()+" End...................\n...........\n");
        
        synchronized(this){
                        tValue.put(Thread.currentThread(), rValue);
                        return rValue;
                        }
        //System.exit(0);
        

    }

    boolean checkContradiction(LinkedList<ALC> nodelabel, ALC newalc) {
        if (newalc.type == Type.atomic) {

            // System.exit(0);
            for (int j = 0; j < nodelabel.size(); j++) {
                if (checkNegation(nodelabel.get(j), newalc) == true) {
                    // System.out.println("Contradiction ...");
                    //System.exit(0);
                    return true;
                }

            }
        }
        if (newalc.type == Type.not) {
            for (int j = 0; j < nodelabel.size(); j++) {
                if (checkNegation(nodelabel.get(j), newalc) == true) {
                    // System.out.println("Contradiction ...");
                    //System.exit(0);
                    return true;
                }

            }
        }


        return false;
    }

    boolean checkNegation(ALC alc1, ALC alc2) {

        if (alc2.type == Type.atomic) {
            //System.out.println("Atomic alc2...");

            if (alc1.type == Type.not) {
                // System.out.println("Not ...");
                //System.exit(0);
                if (alc1.left.type == Type.atomic) {
                    if (alc1.left.name.equals(alc2.name)) {
                        System.out.println(alc1.left.name + " & not " + alc1.left.name);
                        return true;
                    }

                } else {
                    System.out.println("Child of Not is not atomic!!!");
                    System.exit(0);
                }
            }
        }
        if (alc1.type == Type.atomic) {
            if (alc2.type == Type.not) {
                if (alc2.left.type == Type.atomic) {
                    if (alc2.left.name.equals(alc1.name)) {
                        System.out.println(alc2.left.name + " & not " + alc2.left.name);
                        return true;
                    }

                } else {
                    System.out.println("Child of Not is not atomic!!!");
                    System.exit(0);
                }
            }
        }
        return false;

    }

    boolean searchLabel(Gnode node1, ALC new1) {
        ALC alcnew;
        for (int j = 0; j < node1.nodelabel.size(); j++) {
            alcnew = node1.nodelabel.get(j);
            if (alcnew.equals(new1)) {
                return true;
            }
        }
        return false;

    }

    boolean checkSubset(Gnode node1, Gnode node2) {
        if (node1.nodelabel.size() >= node2.nodelabel.size()) {
            for (int i = 0; i < node2.nodelabel.size(); i++) {
                boolean flag = false;
                for (int j = 0; j < node1.nodelabel.size(); j++) {
                    if (node2.nodelabel.get(i).equals(node1.nodelabel.get(j))) {
                        flag = true;
                        break;
                    }
                }
                if (flag == false) {
                    return false;
                }
            }
            return true;
        }
        return false;
    }

    @Override
    public void run() {
        try {


             System.out.println("In child....."+Thread.currentThread().toString()+"\n");

            System.out.println(Thread.currentThread().toString()+" has values as (inside run) "+tList.get(Thread.currentThread()));
           synchronized(this){
            if(tList.get(Thread.currentThread()) == null)
                    {
                         System.out.println("Exception:.. "+Thread.currentThread().toString()+" has values as (inside run) "+tList.get(Thread.currentThread()));
                          System.err.println("Exception:.. "+Thread.currentThread().toString()+" has values as (inside run) "+tList.get(Thread.currentThread()));
                        
          System.exit(0);
                    }
                        
                    }

            //childValue = 
            tableau((LinkedList<Gnode>)tList.get(Thread.currentThread()));
            
            synchronized(this)
            {
                tNum--;
            }
            
        } catch (InterruptedException ex) {
            Logger.getLogger(Project.class.getName()).log(Level.SEVERE, null, ex);
        }
//        throw new UnsupportedOperationException("Not supported yet.");
    }
}